COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the notions of finite union and finite sum
C00003 00003	(proof sums)
C00006 00004	(proof sumfacts)
C00008 ENDMK
C⊗;
;the notions of finite union and finite sum
(wipe-out)
(get-proofs appl prf ekl sys)

(proof sums)

(decl allnum (type: |ground⊗@set→truthval|) (syntype: constant))
(decl somenum (type: |ground⊗@set→truthval|) (syntype: constant))
(decl (numseq f) (type:|ground→ground|))
(decl sum (type: |(@numseq)⊗(@n)→(@n)|) (syntype: constant))
(decl setseq (type: |@n→@set|))
(decl un (type: |(@setseq)⊗(@n)→(@set)|) (syntype: constant))

;axiom for allnum
(defax allnum |∀n a.allnum(0,a)∧(allnum(n',a)≡a(n)∧allnum(n,a))|)
(label allnumdef)

;axiom for somenum
(defax somenum |∀n a.¬somenum(0,a)∧(somenum(n',a)≡a(n)∨somenum(n,a))|)
(label somenumdef)

;axiom for sum
(defax sum |∀n numseq.sum(numseq,0)=0∧sum(numseq,n')=sum(numseq,n)+numseq(n)|)
(label sumdef)

;axiom for un
(defax un |∀n setseq.un(setseq,0)=emptyset∧un(setseq,n')=un(setseq,n)∪setseq(n)|)
(label undef)

(decl disj_pair (syntype: constant) (type: |(@set⊗@set)→truthval|))
(define disj_pair |∀a b.disj_pair(a,b)=emptyp(a∩b)|)
(label disjpair_def)

(decl disjoint (syntype: constant) (type: |((ground→@set)⊗ground)→truthval|))
(defax disjoint |∀n setseq.disjoint(setseq,0)∧
    disjoint(setseq,n')=(disjoint(setseq,n)∧disj_pair(un(setseq,n),setseq(n)))| )
(label disjointdef)
(proof sumfacts)

;properties of allnum and somenum

(axiom |∀a n.(∀m.m<n⊃a(m))≡allnum(n,a)|)
(label allnumfact)

(axiom |∀a n.(∃m.m<n∧a(m))≡somenum(n,a)|)
(label somenumfact)

;properties of un

(axiom |∀setseq n m.m<n⊃setseq(m)⊂un(setseq,n)|)
(label unionfact1)

(axiom |∀u n.n≤length u⊃(un(λm.mkset(nth(u,m)),n))=(λx.(∃k.k<n∧nth(u,k)=x))|)
(label mksetfact)

(axiom |∀u.un(λm.mkset(nth(u,m)),length u)=(λx.(mklset(u))(x))|)
(label mklset_un)

;exercise: unionfact2 
;∀setseq n m.n<m⊃un(setseq,n)⊂un(setseq,m)

;properties of sum

(axiom |∀numseq n.(∀m.m<n⊃natnum(numseq(m)))⊃natnum(sum(numseq,n))|)
(label sumsort)

(save-proofs sums)